Library pedal_triangle
Require Import TrianglesDefs.
Require Import incidence.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Lemma pedal_triangle_ok : ∀ P,
match pedal_triangle P with
(A1,B1,C1) ⇒ perp (line P A1) (line pointB pointC) ∧
perp (line P B1) (line pointA pointC) ∧
perp (line P C1) (line pointA pointB)
end.
Proof.
intros.
destruct P.
simpl. repeat split;
field;auto with triangle_hyps.
Qed.
Lemma cevian_triangle_of_orthocenter_is_pedal :
eq_triangles (cevian_triangle X_4) (pedal_triangle X_4).
Proof.
unfold eq_triangles, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.
Lemma pedal_triangle_of_circumcenter_is_medial :
eq_triangles medial_triangle (pedal_triangle X_3).
Proof.
unfold eq_triangles, medial_triangle, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.
Lemma pedal_triangle_of_incenter_is_intouch :
eq_triangles intouch_triangle (pedal_triangle X_1).
Proof.
unfold eq_triangles, medial_triangle, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.
End Triangle.
Require Import incidence.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Lemma pedal_triangle_ok : ∀ P,
match pedal_triangle P with
(A1,B1,C1) ⇒ perp (line P A1) (line pointB pointC) ∧
perp (line P B1) (line pointA pointC) ∧
perp (line P C1) (line pointA pointB)
end.
Proof.
intros.
destruct P.
simpl. repeat split;
field;auto with triangle_hyps.
Qed.
Lemma cevian_triangle_of_orthocenter_is_pedal :
eq_triangles (cevian_triangle X_4) (pedal_triangle X_4).
Proof.
unfold eq_triangles, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.
Lemma pedal_triangle_of_circumcenter_is_medial :
eq_triangles medial_triangle (pedal_triangle X_3).
Proof.
unfold eq_triangles, medial_triangle, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.
Lemma pedal_triangle_of_incenter_is_intouch :
eq_triangles intouch_triangle (pedal_triangle X_1).
Proof.
unfold eq_triangles, medial_triangle, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.
End Triangle.